Search Results

Documents authored by Aristizábal, Andrés

Document
DOI: 10.4230/LIPIcs.FSCD.2016.9
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Authors: Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.
Cite as

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{aristizabal_et_al:LIPIcs.FSCD.2016.9,
  author =	{Aristiz\'{a}bal, Andr\'{e}s and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr},
  title =	{{Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.9},
  URN =		{urn:nbn:de:0030-drops-59756},
  doi =		{10.4230/LIPIcs.FSCD.2016.9},
  annote =	{Keywords: delimited continuation, dynamic prompt generation, contextual equivalence, environmental bisimulation, up-to technique}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact